Setoid Type Theory—A Syntactic Translation

Altenkirch, Thorsten; Boulier, Simon; Kaposi, Ambrus; Tabereau, Nicolas

Abstract

We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying functional extensionality and propositional extensionality. We justify the rules of setoid type theory by a syntactic translation into a pure type theory with a universe of propositions. We develop the notion of a syntactic translation and relate it to model constructions.

Citation

Altenkirch, T., Boulier, S., Kaposi, A., & Tabereau, N. (2019, October). Setoid Type Theory—A Syntactic Translation. Presented at 13th International Conference on Mathematics of Program Construction (MPC 2019), Porto, Portugal

• Presentation Conference Type: Edited Proceedings
• Conference Name: 13th International Conference on Mathematics of Program Construction (MPC 2019)
• Start Date: Oct 7, 2019
• End Date: Oct 9, 2019
• Acceptance Date: Jun 14, 2019
• Online Publication Date: Oct 20, 2019
• Publication Date: Oct 20, 2019
• Deposit Date: Jan 24, 2020
• Publicly Available Date: Oct 21, 2020
• Publisher: Springer
• Peer Reviewed: Peer Reviewed
• Pages: 155-196
• Series Title: Lecture Notes in Computer Science
• Series Number: 11825
• Series ISSN: 0302-9743
• Book Title: Mathematics of Program Construction: 13th International Conference, MPC 2019, Porto, Portugal, October 7–9, 2019, Proceedings
• ISBN: 9783030336356
• DOI: https://doi.org/10.1007/978-3-030-33636-3_7
• Public URL: https://nottingham-repository.worktribe.com/output/2634853
• Publisher URL: https://link.springer.com/chapter/10.1007/978-3-030-33636-3_7